Repository navigation
feat(lean,#19993): ANALYSE-09-Tuilage-Aperiodique -- pli 5 Origami, famille 155 (FR + jumeau _en) - #19996
Conversation
…55, moteur exact-cover borne, 4 experiences mesurees (FR + jumeau _en) Pli 5 Origami (Part of #19898). Famille 155 openai/math : carreau fini de Z^3 pavant par translations sans aucun pavage totalement periodique (rang 3). Moteur deterministe (backtracking exact-cover + rang du groupe de periodes, elimination gaussienne exacte), quatre experiences mesurees dont deux pieges de fenetre et un theoreme de non-pavage. Copie pedagogique declaree pour l'organe exact-cover (sudoku_lean, lac Lean non invocable depuis Python). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
github-actions
Bot
added
the
markdown-table-syntax
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
[NanoClaw] structural review
VERDICT: LGTM (vérifié: extraction complète protocole v2 FR+_en, chaque valeur du body retrouvée dans les outputs committés, parité code jumeau byte-à-byte)
PR : 4 fichiers, +1393/−0 — 2 carnets neufs (ANALYSE-09-Tuilage-Aperiodique.ipynb +786, jumeau _en +602), README.md +3, _quarto.yml +2. Kernel python3.13, 17 cellules (5 code), exec 1-5 réels.
Vérification par les valeurs (gate #17040) — tout le tableau du body retrouvé à l'identique dans les streams committés :
| Mesure déclarée | Output committé | |
|---|---|---|
| A (4,4,4) 33 nœuds, rang 3, gens (0,1,0)(1,0,0)(0,0,2) | nodes 33 | rang 3 | generateurs [(0, 1, 0), (1, 0, 0), (0, 0, 2)] |
✓ |
| A (6,4,2) 25 nœuds, rang 2 — (0,0,2) invisible (demi-fenêtre z=1) | nodes 25 | rang 2 | generateurs [(0, 1, 0), (1, 0, 0)] |
✓ |
| B0 3 fenêtres, 4-4-5 nœuds, NON RÉSOLU ×3 | nodes 4 / 4 / 5 | NON RESOLU ×3 |
✓ |
| B1 (4,2,2) 9 nœuds rang 2 → (8,2,2) 17 nœuds rang 3, générateur (4,0,0) | nodes 9 | rang 2 puis nodes 17 | rang 3 | … (4, 0, 0) |
✓ |
| B2 (4,4,4) 9 nœuds rang 0 → (8,8,8) 65 nœuds rang 3, 4ℤ³ | nodes 9 | rang 0 | generateurs [] puis nodes 65 | rang 3 | [(0,0,4),(0,4,0),(4,0,0)] |
✓ |
Ce que la mesure ci-dessus valide vraiment : la lecture du §3 et la Conclusion ne citent aucun chiffre absent des outputs. Le raisonnement de la contrainte de main est correct — pour B1, l'équation f(n)+f(n−2)=1 force la phase 4-périodique (f(0)=f(1)=1, f(2)=f(3)=0 ⇒ ∅ n, n−2) et donc une période x minimale exactement 4, cohérente avec le (4,0,0) révélé seulement à (8,2,2) (demi-fenêtre 4). La cohérence des plafonds de demi-fenêtre est vérifiée sur les trois cas (A : ⌊2/2⌋=1 ⟹ (0,0,2) invisible ; B1 : ⌊8/2⌋=4 ⟹ (4,0,0) visible ; B2 idem).
Notebooks — protocole v2 : extraction complète base=∅ (fichiers neufs) → lecture intégrale des cellules markdown (17/17). Exercices : stubs return None + # TODO etudiant avec étapes/indices, aucun raise NotImplementedError/assert False/1/0, aucune cellule solution exécutée. 0 image en sortie (streams seuls) ⇒ aucun base64 dans le contexte. Aucun secret.
Jumeau _en : cellules code byte-identiques au FR (diff des sources code, 0 écart) ; prose réellement traduite (titre, §-titres, table de Conclusion avec les mêmes valeurs). Corps du PR déclare check_twin_parity OK=154/DRIFT=3/MISSING=0 — non re-mesuré par moi (limite assumée de la review structurelle : je ne relance pas les organes CI).
Petits fichiers : README.md = 1 ligne de table (ANALYSE-09, 30 min, description exacte : contre-exemple 3D famille 155, deux pièges de fenêtre, théorème de non-pavage) + 2 lignes d'arbre ; _quarto.yml = 2 entrées FR/_en. Cohérents avec le contenu livré.
Observations non bloquantes : (1) les indices d'exercice nomment le résultat attendu (N₁=8 ; périodes (1,0,0)(0,1,0)(0,0,2)) — atténué car ces valeurs sont déjà imprimées par les outputs du carnet lui-même, donc pas de fuite d'information cachée ; (2) la nav s'ancre sur ANALYSE-04, les 05–08 étant en vol (#19916/#19943/#19962) — re-chaînage post-merge déclaré, geste connu ; (3) statut épistémique honnête (§4 « une fenêtre finie ne prouve jamais l'apériodicité », l'énoncé 155 restant au squelette Lean du corpus) — la limite de mesure est le sujet du carnet, pas un contournement.
[NanoClaw] — review structurelle (protocole v2 : extraction complète FR+_en, diff code intégral, sorties par empreinte et valeur).
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
github-actions
Bot
added
the
consecutive-code-cells
|
Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
|
✅ No unanchored measurement claim detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. The |
|
✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams). Scope = notebooks CHANGED in this PR, not the whole corpus. The |
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
Golden-Set Execution (H.7 P3)✅ 9/9 notebooks passed (certified reproducible)
Pinned lockfile: |
La jambe bloquante check-nav-chain signalait 2 findings orphan_entry imputables au diff : ANALYSE-09 et son jumeau _en n'avaient aucun lien entrant, ce qui portait la serie ANALYSE a trois entrees. Couture, sur le patron deja pose par #19962 (ANALYSE-08) : - ANALYSE-04.Next : Lean-21 -> ANALYSE-09 (la nouvelle tete de serie) ; - ANALYSE-09.Next : -> jumeau _en, qui devient atteignable depuis le FR ; - ANALYSE-09_en.Next : -> index de la serie (README). Aucune cellule de code touchee (markdown de navigation uniquement), donc aucune re-execution due au titre de C.2. Verifie localement : check-notebook-nav-chain rc=0 (0 NEW vs baseline), check-navlinks OK (0 lien casse), twin parity inchangee (OK=154 DRIFT=3 MISSING=0). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
Correctif poussé — La jambe bloquante signalait 2 findings Cause exacte. Couture, sur le patron déjà posé par #19962 (ANALYSE-08) — trois lignes de markdown, aucune cellule de code :
Le FR devient atteignable depuis la chaîne, le jumeau depuis le FR. Aucune cellule de code touchée : pas de ré-exécution due au titre de C.2. Vérifications locales, avant push (worktree du head, pas le checkout partagé) :
Ordre de merge à connaître. #19962 chaîne |
github-actions
Bot
added
the
variation-adjacency-deep-med
github-actions
Bot
added
the
pr-overlap
|
[ADJOINT PREFLIGHT] |
…e sur main (#20058) La PR #19996 a ajoute le jumeau `_en` de `SymbolicAI/Lean/ANALYSE/ANALYSE-09-Tuilage-Aperiodique` sans mettre a jour `EXPECTED_PAIR_COUNT`, qui declare le perimetre decouvert par `discover_pairs()`. La constante est une **egalite**, pas un seuil : le test `test_full_repo_state_passes_parity` rougit dans les deux sens. `main` porte donc `found 9, declared 8` depuis #19996, et la jambe `Scripts Tests (CPU)` est path-filtree sur `scripts/**` : toute PR touchant ce prefixe en herite par construction. Declarer la paire, en documentant son origine dans le bloc de commentaires qui porte deja les huit precedentes. La nouvelle paire est le jumeau `_en` d'un carnet Lean, et non une paire rendue par T4 : la declaration compte le perimetre de `discover_pairs()`, pas une famille de rendu -- le commentaire le dit pour ne pas laisser croire a une neuvieme paire T4. Verifie : le test passe dans un worktree neuf sur `origin/main` (b63b518). La constante etant une egalite, un passage a 9 etablit que `discover_pairs()` en decouvre exactement neuf -- et la meme execution evalue les invariants de contenu de la nouvelle paire, qui sont propres. See #1650 Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
3 participants
Grain: DEEP/notebook-python — lane myia-po-2026:CoursIA — prev: LIGHT/guard #19978
Ce que cette PR livre
Pli 5 Origami (Part of #19898, Closes #19993) :
ANALYSE-09-Tuilage-Aperiodique.ipynb+ jumeau_en, premier carnet de la série sur la famille 155 du corpus openai/math — « A counterexample to periodic tiling in dimension three » : un carreau fini de ℤ³ qui pave par translations sans aucun pavage totalement périodique (groupe de périodes jamais de rang 3 ; des périodes partielles de rang < 3 peuvent exister — nuance portée par le carnet).Contenu : définitions exactes (tuile, couverture exacte, période, rang, périodicité totale) · connexion exact-cover vers
sudoku_lean(ExactCover.IsExactCover) · moteur déterministe (place_tilesbacktracking borné +period_rankpar élimination gaussienne exacte sur ℚ) · quatre expériences mesurées · lecture honnête des limites (§4) · 3 exercices stubbés conformes C.1 · README (ligne table + arbre) +_quarto.yml(entrées FR/_en).Mesures (exécution réelle, kernel python313, artefact end_time 2026-10-08T22:34:56Z, durée 2,30 s, 17 cellules 5 code,
execution_count1-5)Les deux « Lecture du résultat » et le §4 sont ancrés sur ces valeurs mesurées (moteur déterministe : re-jeu = mêmes sorties).
Verdict SOTA : SOTA-OK
Copie pédagogique déclarée pour l'organe exact-cover (
sudoku_lean= lac de preuves Lean, non invocable depuis Python — les 5 questions organ-first sont répondues dans le carnet §2). Le moteur est réel et déterministe ; les fenêtres sont bornées par design pédagogique (0,02 s) et les pièges de mesure (B1, B2) sont le sujet même du carnet, pas des contournements.Conformité
raise NotImplementedError|assert False|1/0(FR et _en) ; stubsreturn None+# TODO étudiantavec étapes et indices.metadata.papermillde l'artefact (chemins au basename, tolérance admise)._en: code byte-identique au FR (source + outputs + ids), prose traduite ;check_twin_parity→ OK=154 DRIFT=3 MISSING=0 (DRIFT=3 = baseline main inchangée).main— les ANALYSE-05..08 sont en vol sur feat(lean,#19908): tranche B pli 2 -- carnet ANALYSE-06 (companion natif des familles 127/132/186/192) #19916/feat(19920,#19898): ANALYSE-07 Percolation-Critique -- pli 3 Origami (tranches A+B) #19943/Feat(lean,#19960): ANALYSE-08 Ramsey/VdW -- enumeration exacte, mur 2^153, pont d'Erdos (pli 4 Origami) #19962 ; le re-chaînage à la consolidation de série est le geste post-merge connu).check_notebook_navlinks: 0 NEW (1495 carnets scannés) ; nav-chain : aucun finding ANALYSE-09.Écart connu (hors périmètre de cette PR)
ANALYSE-08(#19962, en vol) ne porte pas de jumeau_enalors que les plis 3/6/7 en portent — écart de convention repéré pendant ce travail, à traiter sur sa PR ou en suivi, pas ici.🤖 Generated with Claude Code